package trabajoISW2.domain.contracts;

import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Order;
import trabajoISW2.domain.implementations.User;

@Inv("getNumber() > 0 && getNumber().SIZE == 16")
public interface ICreditCard {
	
	@Pre({"type.compareTo(\"\") != 0 #WrongNameException", "type != null #WrongNameException"})
	@Pos("getType().compareTo(type) == 0")
	public void setType(String type);
	
	@Query
	public String getType();
	
	@Pre({"number.length() == 16 #IllegalArgumentException", "number != null"})
	@Pos("getNumber().compareTo(number) == 0")
	public void setNumber(String number);
	
	@Query
	public String getNumber();
	
	@Pre("cvv >= 0 && cvv <=999 #NoPositiveNumberException")
	@Pos({"getCvv() == cvv"})
	public void setCvv(int cvv);
	
	@Query
	public int getCvv();
	
	@Pre({"month > 0 && month <= 12 #IllegalArgumentException"})
	@Pos({"getMonth() == month"})
	public void setMonth(int month);
	
	@Query
	public int getMonth();
	
	@Pre({"year >= 2011 #IllegalArgumentException"})
	@Pos({"getYear() == year"})
	public void setYear(int year);
	
	@Query
	public int getYear();

	@Query
	public List<Order> getOrders();
	
	@Pre("orders !=null #IllegalArgumentException")
	@Pos({"getOrders().equals(orders)"})
	public void setOrders(List<Order> orders);
	
	@Query
	public User getUser();
	
	@Pre("user !=null #IllegalArgumentException")
	@Pos({"getUser().equals(user)"})
	public void setUser(User user);
}
